COMPANION DATA FOR THE PAPER
F. Brandt, C. Geist, and D. Peters. Optimal bounds for the no-show paradox via 
SAT solving. In Proceedings of the 15th International Conference on Autonomous 
Agents and Multi-Agent Systems (AAMAS), pages 314-322. IFAAMAS, 2016.

Prepared by Dominik Peters, dominik.peters@cs.ox.ac.uk
June 2016

-------------------------------------------------------------------------------

The look-up tables that we present here consist of voting rules for 4 alternatives, m = 4. We denote the alternatives as A, B, C, D.

-------------------------------------------------------------------------------

> Theorem 4. There is a Condorcet extension f that satisfies
> participation for m = 4 and n <= 11. Moreover, f is
> pairwise, Pareto-optimal, and a refinement of the top cycle.

The function f described by Theorem 4 is given explicitly in
        good_function_resolute_11.txt
It gives this function as a look-up table. Each row follows the format
        <alternative>,#<voter count>,(<AB>,<AC>,<AD>,<BC>,<BD>,<CD>)
where the 6-tuple at the end specifies a weighted tournament on A, B, C, D, 
where, for example, <AB> is the weight of the arc A -> B. A negative value of 
<AB> would indicate that the arc is directed B -> A. <voter count> is the 
smallest number of voters that suffices to induce this weighted tournament,
this number is not important for understanding the function f. <alternative>
specifies which of A,B,C,D is chosen by f at profiles that induce the given
weighted tournament.
An example row is:
        C,#3,(-1,1,3,-1,3,3)

The python script in
        verify_function_resolute_11.py
reads in the function f from <good_function_resolute_11.txt> and checks that it
satisfies participation.

-------------------------------------------------------------------------------

> Theorem 5. There is a set-valued Condorcet extension F that satisfies 
> optimistic participation for m = 4 and n <= 16, and also is 
> Pareto-optimal and a refinement of the top cycle.

The function F described by Theorem 5 is given explicitly in
        good_function_optimistic_16.txt
It gives this function as a look-up table. Each row follows the format
        <alternative>,#<voter count>,(<AB>,<AC>,<AD>,<BC>,<BD>,<CD>)
where the 6-tuple at the end specifies a weighted tournament on A, B, C, D, 
where, for example, <AB> is the weight of the arc A -> B. A negative value of 
<AB> would indicate that the arc is directed B -> A. <voter count> is a number 
of voters that can induce this weighted tournament.
When given a profile with <voter count> many voters that induces the given 
weighted tournament, the function F chooses the set of all alternatives that
appear as <alternative> in one of these rows. (The rows corresponding to the
same <voter count>,<tournament> pair follow consecutively in the file.)
To save file size, weighted tournaments that have a Condorcet winner are not
listed. Here, F chooses the singleton set consisting of the Condorcet winner.
An example is:
        A,#2,(2,0,0,-2,0,0)
but
        A,#4,(2,0,0,-2,0,0)
        C,#4,(2,0,0,-2,0,0)
        D,#4,(2,0,0,-2,0,0)

The python script in
        verify_function_optimistic_16.py
reads in function F from <good_function_optimistic_16.txt>, complements it 
with Condorcet winners, and checks that it satisfies optimistic participation.

-------------------------------------------------------------------------------

> Theorem 7. There is a set-valued Condorcet extension F that satisfies 
> pessimistic participation for m = 4 and n <= 13.

The function F is described in
        good_function_pessimistic_13.txt
which follows the same data format as in the optimistic case.

To verify, use the script
        verify_function_pessimistic_13.py